Nuprl Definition : d-world 11,40

d-world(D;v;sched;dec;discrete)
== <i,x. M(i).ds(x)
== i,a. M(i).da(locl(a))
== l,tg. M(source(l)).dout(l,tg)
== i,t. if (t = 0)
== then x.M(i).init(x)?v(i,x)
== else (CV(d-comp(Dvscheddecdiscrete))((t - 1),i)).1
== fi 
== i,t. ((CV(d-comp(Dvscheddecdiscrete))(t,i)).2).1
== i,t. (CV(d-comp(Dvscheddecdiscrete))(t,i)).2.2
== i.d-machine(i;M(i);dec(i))
== discrete
== 
latex



clarification:

d-world{i:l}
d-world(Dvscheddecdiscrete)
== <i,x. d-m(Di).ds(x)
== i,a. d-m(Di).da(locl(a))
== l,tg. d-m(D; source(l)).dout(l,tg)
== i,t. if (t = 0)
== then x.d-m(Di).init(x)?v(i,x)
== else (CV(d-comp(Dvscheddecdiscrete))((t - 1),i)).1
== fi 
== i,t. ((CV(d-comp(Dvscheddecdiscrete))(t,i)).2).1
== i,t. (CV(d-comp(Dvscheddecdiscrete))(t,i)).2.2
== i.d-machine(i;d-m(Di);dec(i))
== discrete
== 
latex


DefinitionsM.ds(x), M.da(a), locl(a), M.dout(l,tg), source(l), if b then t else f fi , (i = j), M.init(x)?v, n - m, #$n, t.1, t.2, CV(F), d-comp(Dvscheddecd), x.A(x), d-machine(i;M;dec), M(i), f(a), <ab>,
FDL editor aliasesd-world

origin